ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List),
a:((k:{k:Knd| (k  ks)} decl-state(ds)ma-valtype(da; k)T)), snd:msg-spec(ds; da).
((fpf-dom(id-deq; x; ds)))  (ecl-machine3(ds; da; x; T; ks; a; snd)  es_realizer{i:l}) 

latex

Definitions

Id, t  T, Type, x. t(x), x:A. B(x), fpf(A; a.B(a)), Knd, type List, , x:AB(x), ma-valtype(da; k), decl-state(ds), (x  l), {x:A| B(x)} , , msg-spec(ds; da), x.A(x), top, id-deq, fpf-dom(eq; x; f), b, A, msg-spec-links(snd), idlnk-deq, IdLnk, remove-repeats(eq; L), P  Q, ecl-m3(a; snd; x; l), ecl-tags(l; snd), fpf-single(x; v), fpf-join(eq; f; g), R-lnk-tags(ds; da; l; tgs; ks; g), Rall(L; x.R(x)), ecl-machine3(ds; da; x; T; ks; a; snd)

Lemmas

Rall wf, R-lnk-tags wf, fpf-join wf, fpf-single wf, ecl-tags wf, ecl-m3 wf, remove-repeats wf, IdLnk wf, idlnk-deq wf, msg-spec-links wf, not wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, msg-spec wf, nat wf, l member wf, decl-state wf, ma-valtype wf, bool wf, Knd wf, fpf wf, Id wf